\begin{tabbing} EventsWithOrder \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type\+ \\[0ex]$\times$EqDecider($E$) \\[0ex]$\times$${\it pred?}$:($E$$\rightarrow$($E$+Unit)) \\[0ex]$\times$${\it info}$:($E$$\rightarrow$(Id$\times$Top+(IdLnk$\times$$E$)$\times$Top)) \\[0ex]$\times$EOrderAxioms($E$; ${\it pred?}$; ${\it info}$) \\[0ex]$\times$Top \- \end{tabbing}